Inference at * 
Iof proof for Lemma can-apply-fun-exp-add:


  A:Type, n, m:, f:(A(A + Top)), x:A.
  (can-apply(f^n+m;x))
   {(can-apply(f^m;x))
   & (can-apply(f^n;do-apply(f^m;x)))
   & do-apply(f^n+m;x) = do-apply(f^n;do-apply(f^m;x))} 

latex

 by (Auto') 
CollapseTHEN ((DupHyp (-1)) 
CollapseTHEN (((RWO "p-fun-exp-add" (-1)) 

CoCollapseTHENA (Auto)) 
CollapseTHEN (((FLemma `can-apply-compose` [-1]) 
CollapseTHENA (Auto
C)) 
CollapseTHEN ((Unfold `guard` ( 0)) 
CollapseTHEN ((Auto) 
CollapseTHEN (((
CRWO "p-fun-exp-add" 0) 
CollapseTHENA (Auto)) 
CollapseTHEN ((RWO "do-apply-compose" 0) 

CoCollapseTHEN (Auto)))))))) 

latex

C.

Definitions	, , can-apply(f;x), suptype(S; T), S  T, {T}, , {x:A| B(x)} , , A  B, A, False, P  Q, P & Q, x:A  B(x), s = t, do-apply(f;x), Type, left + right, Top, b, T, True, t  T, P  Q, x:AB(x), f^n, x:A. B(x), P  Q
Lemmas	assert wf, can-apply wf, can-apply-compose, do-apply wf, p-fun-exp-add, do-apply-compose